Basic mathematical structures.md (1553B)
1 +++ 2 title = 'Basic mathematical structures' 3 +++ 4 # Basic mathematical structures 5 ## Type classes 6 7 Different structures: 8 1. semigroups: satisfy `x * (y * z) = (x * y) * z` 9 2. monoids: satisfy 1 above and `x * 1 = x ∧ 1 * x = x` 10 3. groups: satisfy 1 and 2 above, and `x * x⁻¹ = 1 ∧ x⁻¹ * x = 1` 11 12 These are type classes in Lean. 13 14 We can define our own type, integers modulo 2, and register it as an additive group: 15 16 ```lean 17 inductive my_int : Type 18 | zero 19 | one 20 21 def my_int.add : my_int → my_int → my_int 22 | my_int.zero a := a 23 | a my_int.zero := a 24 | my_int.one my_int.one := my_int.zero 25 26 @[instance] def my_int.add_group : add_group my_int := 27 { add := my_int.add, 28 add_assoc := 29 by intros a b c; cases' a; cases' b; cases' c; refl, 30 zero := my_int.zero, 31 zero_add := by intro a; cases' a; refl, 32 add_zero := by intro a; cases' a; refl, 33 neg := λa, a, 34 add_left_neg := by intro a; cases' a; refl } 35 ``` 36 37 ## Lists, multisets, finite sets 38 For finite collections of elements, available structures: 39 - list: order and duplicates matter 40 - multiset: only duplicates matter 41 - finsets: neither order nor duplicates matter 42 43 `dec_trivial` is a lemma you can use for trivial decidable goals (i.e. if there are no variables in the expression). 44 45 ## Order type classes 46 For example `(Ν, ≤)` or `(set Ν, ⊆)`. 47 48 - preorder: reflexivity (`x ≤ x`), transitivity (`x ≤ y → y ≤ z → x ≤ z`) 49 - partial order: preorder with antisymmetry (`x ≤ y → y ≤ x → x = y`) 50 - linear order: partial order with `x ≤ y ∨ y ≤ x`